幽霊型とrank-2 typesで型安全なスコープを作る

幽霊型とrank-2 typesを組み合わせたテクニック

スコープを作るのに使っている？

登場はSTモナドの方が先(90年代)

理解する分には前者のほうがわかりやすいのでは？

モナドがないのでノイズが小さい

code:hs

newtype Named name a = Named a -- nameという幽霊型

type role Named nominal nominal

type a ~~ name = Named name a

name :: a -> (forall name. a ~~ name -> t) -> t

name x k = k (coerce x)

-- 使用する

gdpMain :: IO ()

gdpMain = do

name (comparing Down) $ \gt -> do

let xs' = sortBy gt xs

ys' = sortBy gt ys

print (the (mergeBy gt xs' ys'))

使用する側を見ればわかりやすい

利用者に任意のnameを付けさせずに、nameを与えている

existなnameを指定している感じ

rank-2 typeを使わない場合、以下のような定義になる

code:hs

any_name :: a -> (a ~~ name)

any_name = coerce

しかし、これだと利用者が自在にnameを付けられるため、安全でなくなる

code:hs

newSTRef :: a -> ST s (STRef s a)

runST :: (forall s. ST s a) -> a

runST' :: ST s a -> a -- ダミー. この関数は存在しない.

code:hs

runST $ newSTRef 1 -- error

runST' $ newSTRef 1 -- ok

STモナドの方は2つポイントがある

参照をrunSTの外側に持ち出すことを禁止している

仮に、runSTがrank-1 typeな場合

code:hs

v = runST' (newSTRef "abc") -- v :: STRef s String

foo = runST' (readSTRef v) -- foo :: String == "abc"

-- runST :: (forall s. ST s a) -> a

runST' :: ST s a -> a

runST' st = undefined

参照はmutable変数のようなものなので、モナドの外部に持ち出すと純粋性が失われる

という動作をしている

ST s aのsに具体的な型を指定してしまうとrunSTが使えなくなります。

必ず破壊的な操作にはパラメータ s が多相的なまま残るようになっている．そして， runST はその多相的なまま残った s に対して， s によらずに a の型が決まるならば ST s を外せることにしている．そして， s によらずに a の型が決まる場合に，破壊的操作で生まれた配列のインスタンスやリファレンスが実行時にどのような実体を持っていようとも，結果が決定的になることを保証できるよう， API がうまく設計されている

こう書いたほうが「スコープ感」がわかりやすい？

code:hs

-- ok

ok = runST $ do

n <- newSTRef 0

modifySTRef n (+i)

readSTRef n

code:hs

-- error

ng = runST $ do -- runST $ newSTRef 0 と同じ

n <- newSTRef 0

return n

なぜ幽霊型が必要になるのか？

どこで

存在型との関係

型システム的に高度なことが凝縮されている

rank 2 type

幽霊型

直感的理解

関係ある？